\begin{tabbing}
pre{-}init{-}p2(${\it es}$;$i$;${\it ds}$;${\it init}$;$a$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=pre{-}init{-}p(${\it es}$;$i$;${\it ds}$;${\it init}$;$T$;$P$)\+
\\[0ex]\& pre{-}p(${\it es}$;$i$;${\it ds}$;$a$;$T$;$P$)
\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]fpf{-}dom(IdDeq; $x$; ${\it ds}$)
\\[0ex]$\Rightarrow$ init{-}p(${\it es}$; $i$; fpf{-}ap(${\it ds}$; IdDeq; $x$); $x$; fpf{-}ap(${\it init}$; IdDeq; $x$)))
\-\-
\end{tabbing}